T:Type, eq:EqDecider(T), f:(TT).
retraction(T;f)  (x, y:T. x is f*(y)  (f**(x) = f**(y)  T)) 

latex

Definitions	retraction(T;f), x:AB(x), y is f*(x), s = t, P  Q, x:A. B(x), EqDecider(T), Type, f(a), t  T, , A, f**(x), strong-subtype(A;B), x.A(x), {T}, x,y. t(x;y), P  Q, x:A  B(x), P & Q, P  Q
Lemmas	iff wf, rev implies wf, fix-step, fun-connected-induction, fix wf, not wf, deq wf, fun-connected wf, retraction wf